FDL - Nuprl Lemma : connex_functionality_wrt_iff

Nuprl Lemma : connex_functionality_wrt_iff

T:Type, R, R':(T

T

).
(

x, y:T. R(x,y)

R'(x,y))

(Connex(T;x,y.R(x,y))

Connex(T;x,y.R'(x,y)))

Up rel 1, rel 1

Definitions P Q, P & Q, t T, Connex(T;x,y.R(x;y)), x(s1,s2), P Q, P Q, , x:A. B(x), x. t(x), P Q, x(s)

Lemmas iff wf, or functionality wrt iff, all functionality wrt iff, iff functionality wrt iff